Left Termination proof of /tmp/tmpg5wvXH/ackermann.pl

Left Termination of the query pattern ackermann(b,b,f) w.r.t. the given Prolog program could successfully be proven:

↳ PROLOG

  ↳ PrologToPiTRSProof

ackermann₃(0₀, N, s₁(N)).
ackermann₃(s₁(M), 0₀, Val) :- ackermann₃(M, s₁(0₀), Val).
ackermann₃(s₁(M), s₁(N), Val) :- ackermann₃(s₁(M), N, Val1), ackermann₃(M, Val1, Val).

With regard to the inferred argument filtering the predicates were used in the following modes:
ackermann₃: (b,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

ackermann_3_in_gga₃(0_0, N, s_1₁(N)) -> ackermann_3_out_gga₃(0_0, N, s_1₁(N))
ackermann_3_in_gga₃(s_1₁(M), 0_0, Val) -> if_ackermann_3_in_1_gga₃(M, Val, ackermann_3_in_gga₃(M, s_1₁(0_0), Val))
ackermann_3_in_gga₃(s_1₁(M), s_1₁(N), Val) -> if_ackermann_3_in_2_gga₄(M, N, Val, ackermann_3_in_gga₃(s_1₁(M), N, Val1))
if_ackermann_3_in_2_gga₄(M, N, Val, ackermann_3_out_gga₃(s_1₁(M), N, Val1)) -> if_ackermann_3_in_3_gga₅(M, N, Val, Val1, ackermann_3_in_gga₃(M, Val1, Val))
if_ackermann_3_in_3_gga₅(M, N, Val, Val1, ackermann_3_out_gga₃(M, Val1, Val)) -> ackermann_3_out_gga₃(s_1₁(M), s_1₁(N), Val)
if_ackermann_3_in_1_gga₃(M, Val, ackermann_3_out_gga₃(M, s_1₁(0_0), Val)) -> ackermann_3_out_gga₃(s_1₁(M), 0_0, Val)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

ackermann_3_in_gga₃(0_0, N, s_1₁(N)) -> ackermann_3_out_gga₃(0_0, N, s_1₁(N))
ackermann_3_in_gga₃(s_1₁(M), 0_0, Val) -> if_ackermann_3_in_1_gga₃(M, Val, ackermann_3_in_gga₃(M, s_1₁(0_0), Val))
ackermann_3_in_gga₃(s_1₁(M), s_1₁(N), Val) -> if_ackermann_3_in_2_gga₄(M, N, Val, ackermann_3_in_gga₃(s_1₁(M), N, Val1))
if_ackermann_3_in_2_gga₄(M, N, Val, ackermann_3_out_gga₃(s_1₁(M), N, Val1)) -> if_ackermann_3_in_3_gga₅(M, N, Val, Val1, ackermann_3_in_gga₃(M, Val1, Val))
if_ackermann_3_in_3_gga₅(M, N, Val, Val1, ackermann_3_out_gga₃(M, Val1, Val)) -> ackermann_3_out_gga₃(s_1₁(M), s_1₁(N), Val)
if_ackermann_3_in_1_gga₃(M, Val, ackermann_3_out_gga₃(M, s_1₁(0_0), Val)) -> ackermann_3_out_gga₃(s_1₁(M), 0_0, Val)

ACKERMANN_3_IN_GGA₃(s_1₁(M), 0_0, Val) -> IF_ACKERMANN_3_IN_1_GGA₃(M, Val, ackermann_3_in_gga₃(M, s_1₁(0_0), Val))
ACKERMANN_3_IN_GGA₃(s_1₁(M), 0_0, Val) -> ACKERMANN_3_IN_GGA₃(M, s_1₁(0_0), Val)
ACKERMANN_3_IN_GGA₃(s_1₁(M), s_1₁(N), Val) -> IF_ACKERMANN_3_IN_2_GGA₄(M, N, Val, ackermann_3_in_gga₃(s_1₁(M), N, Val1))
ACKERMANN_3_IN_GGA₃(s_1₁(M), s_1₁(N), Val) -> ACKERMANN_3_IN_GGA₃(s_1₁(M), N, Val1)
IF_ACKERMANN_3_IN_2_GGA₄(M, N, Val, ackermann_3_out_gga₃(s_1₁(M), N, Val1)) -> IF_ACKERMANN_3_IN_3_GGA₅(M, N, Val, Val1, ackermann_3_in_gga₃(M, Val1, Val))
IF_ACKERMANN_3_IN_2_GGA₄(M, N, Val, ackermann_3_out_gga₃(s_1₁(M), N, Val1)) -> ACKERMANN_3_IN_GGA₃(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_3_in_gga₃(0_0, N, s_1₁(N)) -> ackermann_3_out_gga₃(0_0, N, s_1₁(N))
ackermann_3_in_gga₃(s_1₁(M), 0_0, Val) -> if_ackermann_3_in_1_gga₃(M, Val, ackermann_3_in_gga₃(M, s_1₁(0_0), Val))
ackermann_3_in_gga₃(s_1₁(M), s_1₁(N), Val) -> if_ackermann_3_in_2_gga₄(M, N, Val, ackermann_3_in_gga₃(s_1₁(M), N, Val1))
if_ackermann_3_in_2_gga₄(M, N, Val, ackermann_3_out_gga₃(s_1₁(M), N, Val1)) -> if_ackermann_3_in_3_gga₅(M, N, Val, Val1, ackermann_3_in_gga₃(M, Val1, Val))
if_ackermann_3_in_3_gga₅(M, N, Val, Val1, ackermann_3_out_gga₃(M, Val1, Val)) -> ackermann_3_out_gga₃(s_1₁(M), s_1₁(N), Val)
if_ackermann_3_in_1_gga₃(M, Val, ackermann_3_out_gga₃(M, s_1₁(0_0), Val)) -> ackermann_3_out_gga₃(s_1₁(M), 0_0, Val)

The argument filtering Pi contains the following mapping:
ackermann_3_in_gga₃(x1, x2, x3) = ackermann_3_in_gga₂(x1, x2)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
ackermann_3_out_gga₃(x1, x2, x3) = ackermann_3_out_gga₁(x3)
if_ackermann_3_in_1_gga₃(x1, x2, x3) = if_ackermann_3_in_1_gga₁(x3)
if_ackermann_3_in_2_gga₄(x1, x2, x3, x4) = if_ackermann_3_in_2_gga₂(x1, x4)
if_ackermann_3_in_3_gga₅(x1, x2, x3, x4, x5) = if_ackermann_3_in_3_gga₁(x5)
IF_ACKERMANN_3_IN_2_GGA₄(x1, x2, x3, x4) = IF_ACKERMANN_3_IN_2_GGA₂(x1, x4)
IF_ACKERMANN_3_IN_3_GGA₅(x1, x2, x3, x4, x5) = IF_ACKERMANN_3_IN_3_GGA₁(x5)
IF_ACKERMANN_3_IN_1_GGA₃(x1, x2, x3) = IF_ACKERMANN_3_IN_1_GGA₁(x3)
ACKERMANN_3_IN_GGA₃(x1, x2, x3) = ACKERMANN_3_IN_GGA₂(x1, x2)

We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_3_IN_GGA₃(s_1₁(M), 0_0, Val) -> IF_ACKERMANN_3_IN_1_GGA₃(M, Val, ackermann_3_in_gga₃(M, s_1₁(0_0), Val))
ACKERMANN_3_IN_GGA₃(s_1₁(M), 0_0, Val) -> ACKERMANN_3_IN_GGA₃(M, s_1₁(0_0), Val)
ACKERMANN_3_IN_GGA₃(s_1₁(M), s_1₁(N), Val) -> IF_ACKERMANN_3_IN_2_GGA₄(M, N, Val, ackermann_3_in_gga₃(s_1₁(M), N, Val1))
ACKERMANN_3_IN_GGA₃(s_1₁(M), s_1₁(N), Val) -> ACKERMANN_3_IN_GGA₃(s_1₁(M), N, Val1)
IF_ACKERMANN_3_IN_2_GGA₄(M, N, Val, ackermann_3_out_gga₃(s_1₁(M), N, Val1)) -> IF_ACKERMANN_3_IN_3_GGA₅(M, N, Val, Val1, ackermann_3_in_gga₃(M, Val1, Val))
IF_ACKERMANN_3_IN_2_GGA₄(M, N, Val, ackermann_3_out_gga₃(s_1₁(M), N, Val1)) -> ACKERMANN_3_IN_GGA₃(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_3_in_gga₃(0_0, N, s_1₁(N)) -> ackermann_3_out_gga₃(0_0, N, s_1₁(N))
ackermann_3_in_gga₃(s_1₁(M), 0_0, Val) -> if_ackermann_3_in_1_gga₃(M, Val, ackermann_3_in_gga₃(M, s_1₁(0_0), Val))
ackermann_3_in_gga₃(s_1₁(M), s_1₁(N), Val) -> if_ackermann_3_in_2_gga₄(M, N, Val, ackermann_3_in_gga₃(s_1₁(M), N, Val1))
if_ackermann_3_in_2_gga₄(M, N, Val, ackermann_3_out_gga₃(s_1₁(M), N, Val1)) -> if_ackermann_3_in_3_gga₅(M, N, Val, Val1, ackermann_3_in_gga₃(M, Val1, Val))
if_ackermann_3_in_3_gga₅(M, N, Val, Val1, ackermann_3_out_gga₃(M, Val1, Val)) -> ackermann_3_out_gga₃(s_1₁(M), s_1₁(N), Val)
if_ackermann_3_in_1_gga₃(M, Val, ackermann_3_out_gga₃(M, s_1₁(0_0), Val)) -> ackermann_3_out_gga₃(s_1₁(M), 0_0, Val)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_3_IN_GGA₃(s_1₁(M), 0_0, Val) -> ACKERMANN_3_IN_GGA₃(M, s_1₁(0_0), Val)
ACKERMANN_3_IN_GGA₃(s_1₁(M), s_1₁(N), Val) -> ACKERMANN_3_IN_GGA₃(s_1₁(M), N, Val1)
IF_ACKERMANN_3_IN_2_GGA₄(M, N, Val, ackermann_3_out_gga₃(s_1₁(M), N, Val1)) -> ACKERMANN_3_IN_GGA₃(M, Val1, Val)
ACKERMANN_3_IN_GGA₃(s_1₁(M), s_1₁(N), Val) -> IF_ACKERMANN_3_IN_2_GGA₄(M, N, Val, ackermann_3_in_gga₃(s_1₁(M), N, Val1))

The TRS R consists of the following rules:

ackermann_3_in_gga₃(0_0, N, s_1₁(N)) -> ackermann_3_out_gga₃(0_0, N, s_1₁(N))
ackermann_3_in_gga₃(s_1₁(M), 0_0, Val) -> if_ackermann_3_in_1_gga₃(M, Val, ackermann_3_in_gga₃(M, s_1₁(0_0), Val))
ackermann_3_in_gga₃(s_1₁(M), s_1₁(N), Val) -> if_ackermann_3_in_2_gga₄(M, N, Val, ackermann_3_in_gga₃(s_1₁(M), N, Val1))
if_ackermann_3_in_2_gga₄(M, N, Val, ackermann_3_out_gga₃(s_1₁(M), N, Val1)) -> if_ackermann_3_in_3_gga₅(M, N, Val, Val1, ackermann_3_in_gga₃(M, Val1, Val))
if_ackermann_3_in_3_gga₅(M, N, Val, Val1, ackermann_3_out_gga₃(M, Val1, Val)) -> ackermann_3_out_gga₃(s_1₁(M), s_1₁(N), Val)
if_ackermann_3_in_1_gga₃(M, Val, ackermann_3_out_gga₃(M, s_1₁(0_0), Val)) -> ackermann_3_out_gga₃(s_1₁(M), 0_0, Val)

The argument filtering Pi contains the following mapping:
ackermann_3_in_gga₃(x1, x2, x3) = ackermann_3_in_gga₂(x1, x2)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
ackermann_3_out_gga₃(x1, x2, x3) = ackermann_3_out_gga₁(x3)
if_ackermann_3_in_1_gga₃(x1, x2, x3) = if_ackermann_3_in_1_gga₁(x3)
if_ackermann_3_in_2_gga₄(x1, x2, x3, x4) = if_ackermann_3_in_2_gga₂(x1, x4)
if_ackermann_3_in_3_gga₅(x1, x2, x3, x4, x5) = if_ackermann_3_in_3_gga₁(x5)
IF_ACKERMANN_3_IN_2_GGA₄(x1, x2, x3, x4) = IF_ACKERMANN_3_IN_2_GGA₂(x1, x4)
ACKERMANN_3_IN_GGA₃(x1, x2, x3) = ACKERMANN_3_IN_GGA₂(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_3_IN_GGA₂(s_1₁(M), 0_0) -> ACKERMANN_3_IN_GGA₂(M, s_1₁(0_0))
ACKERMANN_3_IN_GGA₂(s_1₁(M), s_1₁(N)) -> ACKERMANN_3_IN_GGA₂(s_1₁(M), N)
IF_ACKERMANN_3_IN_2_GGA₂(M, ackermann_3_out_gga₁(Val1)) -> ACKERMANN_3_IN_GGA₂(M, Val1)
ACKERMANN_3_IN_GGA₂(s_1₁(M), s_1₁(N)) -> IF_ACKERMANN_3_IN_2_GGA₂(M, ackermann_3_in_gga₂(s_1₁(M), N))

The TRS R consists of the following rules:

ackermann_3_in_gga₂(0_0, N) -> ackermann_3_out_gga₁(s_1₁(N))
ackermann_3_in_gga₂(s_1₁(M), 0_0) -> if_ackermann_3_in_1_gga₁(ackermann_3_in_gga₂(M, s_1₁(0_0)))
ackermann_3_in_gga₂(s_1₁(M), s_1₁(N)) -> if_ackermann_3_in_2_gga₂(M, ackermann_3_in_gga₂(s_1₁(M), N))
if_ackermann_3_in_2_gga₂(M, ackermann_3_out_gga₁(Val1)) -> if_ackermann_3_in_3_gga₁(ackermann_3_in_gga₂(M, Val1))
if_ackermann_3_in_3_gga₁(ackermann_3_out_gga₁(Val)) -> ackermann_3_out_gga₁(Val)
if_ackermann_3_in_1_gga₁(ackermann_3_out_gga₁(Val)) -> ackermann_3_out_gga₁(Val)

The set Q consists of the following terms:

ackermann_3_in_gga₂(x0, x1)
if_ackermann_3_in_2_gga₂(x0, x1)
if_ackermann_3_in_3_gga₁(x0)
if_ackermann_3_in_1_gga₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {ACKERMANN_3_IN_GGA₂, IF_ACKERMANN_3_IN_2_GGA₂}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ACKERMANN_3_IN_GGA₂(s_1₁(M), s_1₁(N)) -> ACKERMANN_3_IN_GGA₂(s_1₁(M), N)
The graph contains the following edges 1 >= 1, 2 > 2
ACKERMANN_3_IN_GGA₂(s_1₁(M), s_1₁(N)) -> IF_ACKERMANN_3_IN_2_GGA₂(M, ackermann_3_in_gga₂(s_1₁(M), N))
The graph contains the following edges 1 > 1
IF_ACKERMANN_3_IN_2_GGA₂(M, ackermann_3_out_gga₁(Val1)) -> ACKERMANN_3_IN_GGA₂(M, Val1)
The graph contains the following edges 1 >= 1, 2 > 2
ACKERMANN_3_IN_GGA₂(s_1₁(M), 0_0) -> ACKERMANN_3_IN_GGA₂(M, s_1₁(0_0))
The graph contains the following edges 1 > 1